A, B:Type. A  B  (x, y:A. x = y  B  x = y)  EqDecider(B)  EqDecider(A) 

latex

Definitions	P & Q, S  T, P  Q, S  T, P  Q, EqDecider(T), , P  Q, Prop, b, x:A. B(x), t  T
Lemmas	assert wf, iff wf, bool wf, rev implies wf